<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"
"http://www.w3.org/TR/html4/loose.dtd">

<html>
<head>

<title>
PRISM Manual | FrequentlyAskedQuestions / PRISMProperties 
</title>

<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<meta name="keywords" content="prism, probabilistic, symbolic, model, checker, verification, birmingham, oxford, parker, norman, kwiatkowska">

<link rel="icon" href="../pub/skins/offline/images/p16.ico" type="image/x-icon">
<link rel="shortcut icon" href="../pub/skins/offline/images/p16.ico" type="image/x-icon">

<!--HTMLHeader--><style type='text/css'><!--
  ul, ol, pre, dl, p { margin-top:0px; margin-bottom:0px; }
  code.escaped { white-space: nowrap; }
  .vspace { margin-top:1.33em; }
  .indent { margin-left:40px; }
  .outdent { margin-left:40px; text-indent:-40px; }
  a.createlinktext { text-decoration:none; border-bottom:1px dotted gray; }
  a.createlink { text-decoration:none; position:relative; top:-0.5em;
    font-weight:bold; font-size:smaller; border-bottom:none; }
  img { border:0px; }
  .editconflict { color:green; 
  font-style:italic; margin-top:1.33em; margin-bottom:1.33em; }

  table.markup { border:2px dotted #ccf; width:90%; }
  td.markup1, td.markup2 { padding-left:10px; padding-right:10px; }
  table.vert td.markup1 { border-bottom:1px solid #ccf; }
  table.horiz td.markup1 { width:23em; border-right:1px solid #ccf; }
  table.markup caption { text-align:left; }
  div.faq p, div.faq pre { margin-left:2em; }
  div.faq p.question { margin:1em 0 0.75em 0; font-weight:bold; }
  div.faqtoc div.faq * { display:none; }
  div.faqtoc div.faq p.question 
    { display:block; font-weight:normal; margin:0.5em 0 0.5em 20px; line-height:normal; }
  div.faqtoc div.faq p.question * { display:inline; }
   
    .frame 
      { border:1px solid #cccccc; padding:4px; background-color:#f9f9f9; }
    .lfloat { float:left; margin-right:0.5em; }
    .rfloat { float:right; margin-left:0.5em; }
a.varlink { text-decoration:none; }

.sourceblocklink {
  text-align: right;
  font-size: smaller;
}
.sourceblocktext {
  padding: 0.5em;
  border: 1px solid #808080;
  color: #000000;
  background-color: #f1f0ed;
}
.sourceblocktext div {
  font-family: monospace;
  font-size: small;
  line-height: 1;
  height: 1%;
}
.sourceblocktext div.head,
.sourceblocktext div.foot {
  font: italic medium serif;
  padding: 0.5em;
}

--></style>  <meta name='robots' content='index,follow' />


<link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/base.css">
<link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/prism.css">
<link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/prismmanual.css">

</head>

<body text="#000000" bgcolor="#ffffff">

<div id="layout-maincontainer">
<div id="layout-main">

<div id="prism-mainbox">

<!-- ============================================================================= -->

<!--PageHeaderFmt-->
<!--/PageHeaderFmt-->

<!--PageTitleFmt-->
  <div id="prism-man-title">
    <p><a class='wikilink' href='Main.html'>Frequently Asked Questions</a> /
</p><h1>PRISM Properties</h1>

  </div>
<!--PageText-->
<div id='wikitext'>
<p><a name='mult_states' id='mult_states'></a>
</p><h3>How do I check if a property is true in multiple (or all) states?</h3>
<div class='answer' > 
<p>Consider a typical boolean-valued PRISM property, such as:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock1'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>&lt;<span class="prismnum">0.01</span> [ <span class="prismkeyword">F</span> "<span class="prismident">error</span>" ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='PRISMProperties@action=sourceblock&amp;num=1' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>i.e. "the probability of reaching a state labelled with <code>"error"</code> is less than 0.01. By default, when model checking this query, PRISM will report the result of this property <em>for the initial state</em> of the model, i.e. whether, <em>starting from the initial state</em>, the probability of reaching <code>"error"</code> is below 0.01.
(This is in contrast to older versions of PRISM, which used to report whether the property was true <em>for all</em> states.)
</p>
<p class='vspace'>To check whether the above property is true for, say, all (reachable) states satisfying the label <code>"safe"</code>, you should use <a class='wikilink' href='../PropertySpecification/Filters.html'>filters</a>, as 
illustrated below:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock2'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">filter</span>(<span class="prismident">forall</span>, <span class="prismkeyword">P</span>&lt;<span class="prismnum">0.01</span> [ <span class="prismkeyword">F</span> "<span class="prismident">error</span>" ], "<span class="prismident">safe</span>")<br/>
</div></div>
  <div class='sourceblocklink'><a href='PRISMProperties@action=sourceblock&amp;num=2' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>If you want to check whether the property is true for <em>all</em> reachable states, you can use either of the following two (equivalent) properties:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock3'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">filter</span>(<span class="prismident">forall</span>, <span class="prismkeyword">P</span>&lt;<span class="prismnum">0.01</span> [ <span class="prismkeyword">F</span> "<span class="prismident">error</span>" ], <span class="prismkeyword">true</span>)<br/>
<span class="prismkeyword">filter</span>(<span class="prismident">forall</span>, <span class="prismkeyword">P</span>&lt;<span class="prismnum">0.01</span> [ <span class="prismkeyword">F</span> "<span class="prismident">error</span>" ])<br/>
</div></div>
  <div class='sourceblocklink'><a href='PRISMProperties@action=sourceblock&amp;num=3' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>In older versions of PRISM, checking that a property was true in a particular set of states was done using implication (<code>=&gt;</code>). If you wish, you can still use a similar form of property to achieve this, as shown by the following example: 
</p>
<div class='sourceblock ' id='sourceblock4'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">filter</span>(<span class="prismident">forall</span>, "<span class="prismident">safe</span>" =&gt; <span class="prismkeyword">P</span>&lt;<span class="prismnum">0.01</span> [ <span class="prismkeyword">F</span> "<span class="prismident">error</span>" ])<br/>
</div></div>
  <div class='sourceblocklink'><a href='PRISMProperties@action=sourceblock&amp;num=4' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

</div>
<p class='vspace'><a name='action' id='action'></a>
</p><h3>How do I compute the probability of an action occurring?</h3>
<div class='answer' > 
<p>PRISM's property specification language is primarily state-based, e.g. you can compute the probability of reaching a <em>state</em> that satisfies the label <code>"error"</code>:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock5'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span> "<span class="prismident">error</span>" ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='PRISMProperties@action=sourceblock&amp;num=5' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>So how do you compute the probability of a some action <code>b</code> occurring? You need to make a small change to your model. The cleanest way to do this is to add a small module that changes state when the action occurs, e.g.:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock6'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">module</span> <span class="prismident">checker</span><br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="prismident">q</span> : [<span class="prismnum">0</span>..<span class="prismnum">1</span>] <span class="prismkeyword">init</span> <span class="prismnum">0</span>;<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;[<span class="prismident">b</span>] <span class="prismident">q</span>=<span class="prismnum">0</span> -&gt; (<span class="prismident">q</span>'=<span class="prismnum">1</span>);<br/>
&nbsp;&nbsp;&nbsp;&nbsp;[<span class="prismident">b</span>] <span class="prismident">q</span>=<span class="prismnum">1</span> -&gt; (<span class="prismident">q</span>'=<span class="prismnum">1</span>);<br/>
<br/>
<span class="prismkeyword">endmodule</span><br/>
</div></div>
  <div class='sourceblocklink'><a href='PRISMProperties@action=sourceblock&amp;num=6' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>You can determine the probability of action <code>b</code> occurring in the model with the property:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock7'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span> <span class="prismident">q</span>=<span class="prismnum">1</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='PRISMProperties@action=sourceblock&amp;num=7' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>By design, the module above will not affect the behaviour (timing, probability, etc.) of your model at all, so all other properties will remain unchanged. This is true for any of the model types that PRISM supports. It may, though, lead to a (hopefully small) increase in total model size.
</p>
<p class='vspace'>You can also modify the property above to compute, for example, the probability of <code>b</code> occurring within <code>T</code> time-units or the expected time until <code>b</code> occurs:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock8'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span>&lt;=<span class="prismident">T</span> <span class="prismident">q</span>=<span class="prismnum">1</span> ]<br/>
<span class="prismkeyword">R</span>{"<span class="prismident">time</span>"}=? [ <span class="prismkeyword">F</span> <span class="prismident">q</span>=<span class="prismnum">1</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='PRISMProperties@action=sourceblock&amp;num=8' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>(where a constant <code>T</code> or reward structure <code>time</code> have been added to the model, as appropriate).
</p></div>
</div>


<!--PageFooterFmt-->
  <div id='prism-man-footer'>
  </div>
<!--/PageFooterFmt-->


<!-- ============================================================================= -->

</div> <!-- id="prism-mainbox" -->

</div> <!-- id="layout-main" -->
</div> <!-- id="layout-maincontainer" -->

<div id="layout-leftcol">
<div id="prism-navbar2">

<h3><a class='wikilink' href='../Main/Welcome.html'>PRISM Manual</a></h3>
<p><strong><a class='wikilink' href='Main.html'>Frequently Asked Questions</a></strong>
</p><ul><li><a class='wikilink' href='MemoryProblems.html'>Memory Problems</a>
</li><li><a class='wikilink' href='PRISMModelling.html'>PRISM Modelling</a>
</li></ul><p>[ <a class='wikilink' href='AllOnOnePage.html'>View all</a> ]
</p>


</div>  <!-- id="prism-navbar2" -->
</div> <!-- id="layout-leftcol" -->

</body>
</html>
